-module(prop_psm).

-include_lib("proper/include/proper.hrl").
-include("../src/rtps.hrl").
-include("../src/rtps_psm.hrl").

-export([bin_float32/0, ascii/0, enums/0]).

%%%%%%%%%%%%%%%%%%
%%% Properties %%%
%%%%%%%%%%%%%%%%%%

%% IIOP 1.0
prop_short() ->
    ?FORALL(X, choose(?SHORTMIN, ?SHORTMAX),
	    begin
		{X, _} = rtps_psm:dec_short(big, rtps_psm:enc_short(X)),
		true
	    end).

prop_unsigned_short() ->
    ?FORALL(X, choose(?USHORTMIN, ?USHORTMAX),
	    begin
		{X, _} = rtps_psm:dec_unsigned_short(big, rtps_psm:enc_unsigned_short(X)),
		true
	    end).

prop_long() ->
    ?FORALL(X, choose(?LONGMIN, ?LONGMAX),
	    begin
		{X, _} = rtps_psm:dec_long(big, rtps_psm:enc_long(X)),
		true
	    end).

prop_unsigned_long() ->
    ?FORALL(X, resize(?ULONGMAX, choose(?ULONGMIN, ?ULONGMAX)),
	    begin
		{X, _} = rtps_psm:dec_unsigned_long(big, rtps_psm:enc_unsigned_long(X)),
		true
	    end).

prop_bool() ->
    ?FORALL(X, boolean(),
	    begin
		{X, _} = rtps_psm:dec_bool(rtps_psm:enc_bool(X)),
		true
	    end).

prop_float() ->
    ?FORALL(X, bin_float32(),
	    begin
		%% Go the other way round, start with the binary,
		%% convert it to a float and back again. This is
		%% because generating 32 bit floats is tricky.
		{F, _} = rtps_psm:dec_float(big, X),
                X = rtps_psm:enc_float(F),
		true
	    end).

prop_double() ->
    ?FORALL(X, float(),
	    begin
		{X, _} = rtps_psm:dec_double(big, rtps_psm:enc_double(X)),
		true
	    end).

prop_char() ->
    ?FORALL(X, choose(0, 255),
	    begin
		{X, _} = rtps_psm:dec_char(rtps_psm:enc_char(X)),
		true
	    end).

prop_octet() ->
    ?FORALL(X, choose(0, 255),
	    begin
		{X, _} = rtps_psm:dec_octet(rtps_psm:enc_octet(X)),
		true
	    end).

prop_string() ->
    ?FORALL(X, ascii(),
	    begin
		{X, _} = rtps_psm:dec_string(big, rtps_psm:enc_string(X)),
		true
	    end).

prop_enum() ->
    ?FORALL({X, Enums}, enums(),
	    begin
		{X, _} = rtps_psm:dec_enum(big, Enums, rtps_psm:enc_enum(X, Enums)),
		true
	    end).

prop_sequence() ->
    ?FORALL(X, binary(),
	    begin
		{X, _} = rtps_psm:dec_sequence(big, rtps_psm:enc_sequence(X)),
		true
	    end).

prop_longlong() ->
    ?FORALL(X, choose(?LONGLONGMIN, ?LONGLONGMAX),
	    begin
		{X, _} = rtps_psm:dec_longlong(big, rtps_psm:enc_longlong(X)),
		true
	    end).

prop_unsigned_longlong() ->
    ?FORALL(X, choose(?ULONGLONGMIN, ?ULONGLONGMAX),
	    begin
		{X, _} = rtps_psm:dec_unsigned_longlong(big, rtps_psm:enc_unsigned_longlong(X)),
		true
	    end).

%% RTPS

prop_guid() ->
   ?FORALL(X, ?SUCHTHAT(X, rtps:guid(), X =/= unknown),
	    begin
		X = rtps_psm:dec_guid(rtps_psm:enc_guid(X)),
		true
	    end).

prop_guid_prefix() ->
    ?FORALL(X, rtps:guid_prefix(),
	    begin
		{X, _} = rtps_psm:dec_guid_prefix(rtps_psm:enc_guid_prefix(X)),
		true
	    end).

prop_entity_id() ->
    ?FORALL(X, rtps:entity_id(),
	    begin
		{X, _} = rtps_psm:dec_entity_id(rtps_psm:enc_entity_id(X)),
		true
	    end).

prop_vendor() ->
    ?FORALL(X, rtps:vendor_id(),
	    begin
		{X, _} = rtps_psm:dec_vendor(rtps_psm:enc_vendor(X)),
		true
	    end).

prop_prot_ver() ->
    ?FORALL(X, rtps:protocol_version(),
	    begin
		{X, _} = rtps_psm:dec_prot_ver(rtps_psm:enc_prot_ver(X)),
		true
	    end).

prop_sequence_number() ->
    ?FORALL(X, rtps:sequence_number(),
	    begin
		{X, _} = rtps_psm:dec_sn(big, rtps_psm:enc_sn(X)),
		true
	    end).

prop_sequence_number_set() ->
    ?FORALL(X, snset(sn(rtps:sequence_number()), choose(1, ?MAX_NS_SIZE)),
	    begin
		{X, _} = rtps_psm:dec_snset(big, rtps_psm:enc_snset(X)),
		true
	    end).

prop_fragment_number() ->
    ?FORALL(X, rtps:fragment_number(),
	    begin
		{X, _} = rtps_psm:dec_fn(big, rtps_psm:enc_fn(X)),
		true
	    end).

prop_fragment_number_set() ->
    ?FORALL(X, fnset(rtps:fragment_number(), choose(1, ?MAX_NS_SIZE)),
	    begin
		{X, _} = rtps_psm:dec_fnset(big, rtps_psm:enc_fnset(X)),
		true
	    end).

prop_time() ->
    ?FORALL(X, rtps:time(),
	    begin
		case X of
		    #time{seconds = 0, fraction = 0} ->
			{zero, _} = rtps_psm:dec_time(big, rtps_psm:enc_time(X));
		    _ ->
			{X, _} = rtps_psm:dec_time(big, rtps_psm:enc_time(X))
		end,
		true
	    end).

prop_loc() ->
    ?FORALL(X, loc(rtps:locator()),
	    begin
		{X, _} = rtps_psm:dec_loc(big, rtps_psm:enc_loc(X)),
		true
	    end).

prop_locudpv4() ->
    ?FORALL(X, rtps:locator_udpv4(),
	    begin
		{X, _} = rtps_psm:dec_locudpv4(big, rtps_psm:enc_locudpv4(X)),
		true
	    end).

prop_locl() ->
    ?FORALL(X, non_empty(list(loc(rtps:locator()))),
	    begin
		L1 = lists:sort(X),
		{L2, _} = rtps_psm:dec_locl(big, rtps_psm:enc_locl(X)),
		L1 =:= lists:sort(L2)
	    end).

%% TODO: Make this work: testing goes wrong when a set contains the
%% same value mre than once since the set is returned with a single
%% entry.
%% prop_parameter_list() ->
%%     ?FORALL(X, list(rtps:parameter()),
%% 	    begin
%% 		L1 = lists:sort(X), {L2, _} = rtps_psm:dec_parl(big,  rtps_psm:enc_parl(L1)),
%% 		L1 =:= lists:sort(L2)
%% 	    end).


%%%%%%%%%%%%%%%
%%% Helpers %%%
%%%%%%%%%%%%%%%

to_range(M, N) ->
    Base = N div M,
    {Base * M, (Base + 1) * M}.

set(Base, N) ->
    [Base + Offset || Offset <- lists:seq(0, N - 1), rand:uniform(2) =/= 1].    

%%%%%%%%%%%%%%%%%%
%%% Generators %%%
%%%%%%%%%%%%%%%%%%

bin_float32() ->
    ?LET(X, float(), <<X:32/big-float>>).

ascii() ->
    ?LET(X, binary(), binary_to_list(X)).
    
enums() ->
    ?LET({T, L1, L2}, {term(), list(term()), list(term())}, {T, L1 ++ [T] ++ L2}).

sn(Gen) ->
    ?SUCHTHAT(Sn, Gen, Sn =/= unknown).

snset(Sn_generator, Num_bits_generator) ->
    ?LET({Base, N}, {Sn_generator, Num_bits_generator},
	 begin
	     Set = set(Base, N),
	     #sequence_number_set{base = Base, set = Set, num_bits = N}
	 end).

fnset(Fn_generator, Num_bits_generator) ->
    ?LET({Base, N}, {Fn_generator, Num_bits_generator},
	 begin
	     Set = set(Base, N),
	     #fragment_number_set{base = Base, set = Set, num_bits = N}
	 end).

loc(Gen) ->
    ?SUCHTHAT(Loc, Gen, Loc =/= invalid).

